Nuprl Lemma : mon_itop_unroll_lo
13,42
postcript
pdf
g
:IMonoid,
i
,
j
:
.
(
i
<
j
)
(
E
:({
i
..
j
}
|
g
|). (
i
k
<
j
.
E
(
k
)) = (
E
(
i
) * (
i
+1
k
<
j
.
E
(
k
)))
|
g
|)
latex
Up
groups
1
Definitions of Statement
lb
i
<
ub
.
E
(
i
)
Definitions
lb
i
<
ub
.
E
(
i
)
Lemmas
itop
unroll
lo
origin